class Factorial {
    public static void main() {
    	Test t;
        t=new Test();
        t.f(1);
    	
    }    

}

class Test {
	int a ;
	int b ;
	public int f1(int x,int y){
        pre: (a+2)*(b+1)>b;
        post: a<b;
    	int c;
    	a=1;
    	b=2;
    	c=a+b;
    	if (a>b) {
            c=1;
        }
        else {
            c=2;
        }
        while (a<5){
            b=b+1;
        }
        return c;		
	}
	public int f1(int x){
        pre: (a+2)*(b+1)>b;
        post: a<b;
    	int c;
    	a=1;
    	b=2;
        while (a<5){
            b=b+1;
        }
        return c;		
	}	
    public int f(long x){
        pre: (a+2)*(b+1)>b;
        post: a<b;
    	int c;
    	a=1;
    	b=2;
    	c=a+b;
    	if (a>b) {
            c=1;
        }
        else {
            c=2;
        }
        while (a<5){
            b=b+1;
        }
        c=f1(a);
        c=f1(a,b);
        return c;
    }
    
}

class TestE extends Test{
	int lauth;
}
    